COMMENT ⊗   VALID 00003 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	(DEFPROP POSBIT 
 00003 00003	(DEFPROP RESOLVE 
 00006 ENDMK
⊗;
(DEFPROP POSBIT 
 (LAMBDA (X) (LIST (QUOTE CADAAR) (CADR X))) 
MACRO)

(DEFPROP NEGBIT 
 (LAMBDA (X) (LIST (QUOTE CDDAAR) (CADR X))) 
MACRO)

(DEFPROP NEGL 
 (LAMBDA (C) (LIST (QUOTE CADAR) (CADR C))) 
MACRO)
(DEFPROP RESOLVE 
 (LAMBDA(C D)
  (COND ((OR (ALLNEG D) (ALLPOS C)) (RESOLVE1 C D))
	((OR (ALLPOS D) (ALLNEG C)) (RESOLVE1 D C))
	(T (NCONC (RESOLVE1 C D) (RESOLVE1 D C))))) 
EXPR)

(DEFPROP RESOLVE1 
 (LAMBDA(C D)
  (PROG (CB DB DB1 YC YD YD1 Z X Y RES)
	(SETQ YC (CDR C))
	(SETQ CB (POSBIT C))
	(SETQ YD1 (NEGL D))
	(SETQ DB1 (NEGBIT D))
	(SETQ DB DB1)
	(SETQ YD YD1)
   RES1 (SETQ X (CAR YC))
	(COND ((NEG X) (RETURN RES)))
	(SETQ Y (CAR YD))
	(COND ((ORDERP (CAR X) (CADR Y)) (GO RES3)) ((NOT (EQ (CAR X) (CADR Y))) (GO RES4)))
	(SETQ YD1 YD)
	(SETQ DB1 DB)
	(GO RES2A)
   RES2 (SETQ Y (CAR YD))
	(COND ((NOT (EQ (CAR X) (CADR Y))) (GO RES3A)))
   RES2A
	(COND ((NOT (UNIFAB (CAR CB) (CAR DB))) (GO RES2B)))
	(SETQ Z (UNIFY (CDR X) (CDDR Y)))
	(COND ((NULL Z) (GO RES2B)))
	(SETQ PARRES NIL)
	(SETQ Z (UNION (CDR Z) C D X Y))
	(COND ((NULL Z) (GO RES2B)) ((NULL (CAR Z)) (RETURN Z)))
	(SETQ RES (CONS (SET2 (CAR (COND (DLIST (DEMOD Z DLIST)) (EQUAL (ORDEREQUAL1 Z)) (T Z))) TBL) RES))
   RES2B
	(SETQ YD (CDR YD))
	(COND (YD (SETQ DB (CDR DB)) (GO RES2)))
   RES3A
	(SETQ DB DB1)
	(SETQ YD YD1)
   RES3 (SETQ YC (CDR YC))
	(COND (YC (SETQ CB (CDR CB)) (GO RES1)))
	(RETURN RES)
   RES4 (SETQ YD (CDR YD))
	(COND (YD (SETQ DB (CDR DB)) (GO RES1)))
	(GO RES3A))) 
EXPR)